package com.googlecode.kipler.satisfiability.completion.strategy;

import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;

import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.World;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.container.dl.operational.FilterType;
import com.googlecode.kipler.container.dl.operational.RelatedIndividualWithTypeFilter;
import com.googlecode.kipler.container.dl.operational.RelatedIndividualWithTypeFilterFactory;
import com.googlecode.kipler.satisfiability.blocking.abox.ABoxBlockingStrategy;
import com.googlecode.kipler.satisfiability.blocking.abox.SubsetBlocking;
import com.googlecode.kipler.satisfiability.completion.rule.CompletionRule;
import com.googlecode.kipler.satisfiability.completion.rule.EmptyDomainRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.AlwaysFormulaRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.AndRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.BeforeFormulaRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.OrRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.SometimeFormulaRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.UntilFormulaRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.ABoxRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.AllValuesRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.AlwaysConceptRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.BeforeConceptRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.IntersectionRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.LazyUnfoldingRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.NegatedConceptDefinitionRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.PositiveConceptDefinitionRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.SomeValuesRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.SometimeConceptRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.UnionRule;
import com.googlecode.kipler.satisfiability.completion.rule.individual.UntilConceptRule;
import com.googlecode.kipler.satisfiability.reasoner.Reasoner;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;


public class LTLALCCompletionStrategy implements CompletionStrategy {
	private List<CompletionRule> formulaRuleList = new ArrayList<CompletionRule>();

	private List<ABoxRule> generatingRuleList = new ArrayList<ABoxRule>();

	private List<ABoxRule> labelModifyingRuleList = new ArrayList<ABoxRule>();

	private Reasoner reasoner;

	private World currentWorld;

	private WorldConstraintSystem currentWcs;

	public LTLALCCompletionStrategy(Reasoner reasoner) {
		setReasoner(reasoner);

		formulaRuleList.add(new AndRule());
		formulaRuleList.add(new AlwaysFormulaRule());
		formulaRuleList.add(new BeforeFormulaRule());
		formulaRuleList.add(new OrRule(reasoner));
		formulaRuleList.add(new SometimeFormulaRule(getReasoner()));
		formulaRuleList.add(new UntilFormulaRule(getReasoner()));

		ABoxBlockingStrategy blocking = new SubsetBlocking();
		RelatedIndividualWithTypeFilter filterer = RelatedIndividualWithTypeFilterFactory
				.getFilter(FilterType.TYPED_SUCCESSOR);
		labelModifyingRuleList.add(new LazyUnfoldingRule());
		labelModifyingRuleList.add(new PositiveConceptDefinitionRule(blocking));
		labelModifyingRuleList.add(new IntersectionRule(blocking));
		labelModifyingRuleList.add(new AlwaysConceptRule(blocking));
		labelModifyingRuleList.add(new BeforeConceptRule(blocking));
		labelModifyingRuleList.add(new AllValuesRule(blocking));
		labelModifyingRuleList.add(new UnionRule(getReasoner(), blocking));
		labelModifyingRuleList.add(new SometimeConceptRule(getReasoner(),
				blocking));
		labelModifyingRuleList
				.add(new UntilConceptRule(getReasoner(), blocking));

		generatingRuleList.add(new SomeValuesRule(blocking, filterer, false));
	}

	/**
	 * @return the reasoner
	 */
	public Reasoner getReasoner() {
		return reasoner;
	}

	/**
	 * @param reasoner
	 *            the reasoner to set
	 */
	public void setReasoner(Reasoner reasoner) {
		this.reasoner = reasoner;
	}

	public void apply(WorldConstraintSystem currentWcs)
			throws ReasonerException {
		currentWorld = currentWcs.worldIterator().next();
		this.currentWcs = currentWcs;
		applyFormulaRules();
		applyABoxRules();
	}

	private void applyFormulaRules() throws ReasonerException {
		while (new RuleApplication(currentWcs, currentWorld)
				.applySingleFormulaRule(formulaRuleList))
			;
	}

	private void applyABoxRules() throws ReasonerException {
		CompletionRule compRule = new NegatedConceptDefinitionRule(currentWcs,
				currentWorld);
		compRule.apply();
		compRule = new EmptyDomainRule(currentWcs, currentWorld);
		compRule.apply();
		do {
			applyLabelModifyingRules();
		} while (applyGeneratingRules());
	}

	private void applyLabelModifyingRules() throws ReasonerException {
		boolean ruleApplied;
		do {
			ruleApplied = false;
			Iterator<Individual> indvIter = currentWorld.getABox()
					.individualIterator();
			while (indvIter.hasNext()) {
				Individual indv = indvIter.next();
				while (new RuleApplication(currentWcs, currentWorld)
						.applySingleIndividualRule(labelModifyingRuleList, indv)) {
					ruleApplied = true;
				}
			}
		} while (ruleApplied);
	}

	private boolean applyGeneratingRules() throws ReasonerException {
		return applyARuleFromRuleListToIndv(generatingRuleList);
	}

	private boolean applyARuleFromRuleListToIndv(List<ABoxRule> ruleList)
			throws ReasonerException {
		boolean ruleApplied = false;
		Iterator<Individual> indvIter = currentWorld.getABox()
				.individualIterator();
		while (indvIter.hasNext() && !ruleApplied) {
			Individual indv = indvIter.next();
			ruleApplied = new RuleApplication(currentWcs, currentWorld)
					.applySingleIndividualRule(ruleList, indv);
		}
		return ruleApplied;
	}

}
